Automated deduction in additive and multiplicative linear logic
Identifieur interne : 00D690 ( Main/Exploration ); précédent : 00D689; suivant : 00D691Automated deduction in additive and multiplicative linear logic
Auteurs : Didier Galmiche [France] ; Guy Perrier [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: In this work we consider the additive and multiplicative linear logic (AMLL) with an automated deduction point of view. Considering this recent logical framework and its possible extensions or applications to logic programming, programming with proofs or parallelism and concurrency, we propose a new algorithm that constructs a proof for a given sequent in AMLL and its termination, correctness and completeness proofs. It can be viewed as a direct (or constructive) proof of the decidability of AMLL and as a first step to consider linear logic as a basis for an extended programming logic. The restriction (and adaptation) of this result to multiplicative linear logic (MLL) gives an adequate algorithm for automatic proof net construction.
Url:
DOI: 10.1007/BFb0023870
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000300
- to stream Istex, to step Curation: 000299
- to stream Istex, to step Checkpoint: 003030
- to stream Main, to step Merge: 00DF67
- to stream Main, to step Curation: 00D690
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automated deduction in additive and multiplicative linear logic</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name></author><author><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:0DC522221F274EECDB94B56B1412F2885318F248</idno><date when="1992" year="1992">1992</date><idno type="doi">10.1007/BFb0023870</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-P8470QG1-0/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000300</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000300</idno><idno type="wicri:Area/Istex/Curation">000299</idno><idno type="wicri:Area/Istex/Checkpoint">003030</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">003030</idno><idno type="wicri:doubleKey">0302-9743:1992:Galmiche D:automated:deduction:in</idno><idno type="wicri:Area/Main/Merge">00DF67</idno><idno type="wicri:Area/Main/Curation">00D690</idno><idno type="wicri:Area/Main/Exploration">00D690</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automated deduction in additive and multiplicative linear logic</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Campus Scientifique, CRIN-CNRS-INRIA Lorraine, B.P. 239, 54506, Vandoeuvre-les-Nancy Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Campus Scientifique, CRIN-CNRS-INRIA Lorraine, B.P. 239, 54506, Vandoeuvre-les-Nancy Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In this work we consider the additive and multiplicative linear logic (AMLL) with an automated deduction point of view. Considering this recent logical framework and its possible extensions or applications to logic programming, programming with proofs or parallelism and concurrency, we propose a new algorithm that constructs a proof for a given sequent in AMLL and its termination, correctness and completeness proofs. It can be viewed as a direct (or constructive) proof of the decidability of AMLL and as a first step to consider linear logic as a basis for an extended programming logic. The restriction (and adaptation) of this result to multiplicative linear logic (MLL) gives an adequate algorithm for automatic proof net construction.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name></region><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00D690 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00D690 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:0DC522221F274EECDB94B56B1412F2885318F248
|texte= Automated deduction in additive and multiplicative linear logic
}}
| This area was generated with Dilib version V0.6.33. |  |